\begin{tabbing}
EOrder\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type$_{\mbox{\scriptsize i}}$\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$${\it pred?}$:($E$$\rightarrow$($E$+Unit))
\\[0ex]$\times$${\it info}$:($E$$\rightarrow$(Id$\times$Top+(IdLnk$\times$$E$)$\times$Top))
\\[0ex]$\times$EO\=rderAxioms\{i\}($E$;\+
\\[0ex]${\it pred?}$;
\\[0ex]${\it info}$)
\-\\[0ex]$\times$Top
\-
\end{tabbing}